(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/pts.ma".
include "basics/types.ma".
include "basics/bool.ma".

(* Notation:
  τ   = tau
  ↑ ↓ = uarr darr
  ø • = oslash bullet
  〘 〙 = lopar ropar
  ⌊ ⌋ = lfloor rfloor
  ▹ │ = rtri boxv
*)



(* <<< Action definition >>> *)
inductive lab (L:Type[0]): Type[0] ≝
  | pos: L → lab L            (* actions    *)
  | neg: L → lab L.           (* co-actions *)

inductive act (L:Type[0]): Type[0] ≝
  | tau: act L                (* syncronization *)
  | ava: lab L → act L.       (* all visible actions *)

notation "τ" non associative with precedence 90 for @{'tau_act}.
interpretation "sync" 'tau_act = (tau ?).

notation "↑a" non associative with precedence 90 for @{'pos_act $a}.
interpretation "pos_act" 'pos_act a = (ava ? (pos ? a)).

notation "↓a" non associative with precedence 90 for @{'neg_act $a}.
interpretation "neg_act" 'neg_act a = (ava ? (neg ? a)).



(* <<< Process definition >>> *)
inductive proc (L:Type[0]) (A:act L): Type[0] ≝
    nil: proc L A                              (*  nil     *)
  | pre: act L → proc L A → proc L A           (*  a.P     *)
  | sum: proc L A → proc L A → proc L A        (*  P + Q   *)
  | par: proc L A → proc L A → proc L A        (*  P | Q   *)
  | res: proc L A → lab L → proc L A           (*  P\{a}   *)
  | rel: proc L A → lab L → act L → proc L A.  (*  P[x/b]  *)

notation "ø" non associative with precedence 90 for @{'nil_proc}.
interpretation "nil" 'nil_proc = (nil ??).

notation "P〘a〙" non associative with precedence 85 for @{'res_proc $P $a }.
interpretation "res_proc" 'res_proc P a = (res ?? P a).  

notation "P⌊a▹b⌋" non associative with precedence 80 for @{'rel_proc $P $a $b}.
interpretation "rel_proc" 'rel_proc P a b = (rel ?? P a b).

notation "a•P" non associative with precedence 75 for @{'pre_proc $a $P}.
interpretation "pre_proc" 'pre_proc a P = (pre ?? a P).

notation "P│Q" left associative with precedence 70 for @{'par_proc $P $Q}.
interpretation "par_proc" 'par_proc P Q = (par ?? P Q).

notation "P+Q" left associative with precedence 65 for @{'sum_proc $P $Q}.
interpretation "sum_proc" 'sum_proc P Q = (sum ?? P Q).



(* <<< Structural Operational Semantics >>> *)
(* To generate co-action *)
let rec coact (L:Type[0]) (a:act L) on a: act L ≝
  match a with [
      tau   ⇒ a
    | ava x ⇒ match x with
                [ pos b ⇒ (ava ? (neg ? b)) | neg b ⇒ (ava ? (pos ? b)) ]
  ].

(* To compare actions *)
let rec eqact (L:Type[0]) (a,b:act L) on a: Prop ≝
  match a with [
      tau   ⇒ False
    | ava x ⇒ match x with [
                  pos c ⇒ match b with [
                              tau ⇒ False
                            | ava y ⇒ match y with [
                                          pos d ⇒ (c = d)
                                        | neg d ⇒ (c = d) ]
                          ]
                | neg c ⇒ match b with [
                              tau ⇒ False
                            | ava y ⇒ match y with [
                                          pos d ⇒ (c = d)
                                        | neg d ⇒ (c = d) ]
                          ]
              ]
  ].

(* To rewrite label (if a==x then b else a) *)
let rec rewact (L:Type[0]) (a,b:act L) (x:lab L) on a: act L ≝
  match a with [
      tau   ⇒ a
    | ava y ⇒ match y with [
                  pos c ⇒ match x with [ pos c ⇒ b | _ ⇒ a ]
                | neg c ⇒ match x with [ neg c ⇒ b | _ ⇒ a ]
              ]
  ].

(* Transition *)
inductive trans (L:Type[0]) (A:act L): proc L A → act L → proc L A → Prop ≝
    tnil:  ∀P.   trans L A P τ P                          (*    P ─τ→ P       *)
  | tpre:  ∀P,a. trans L A (a•P) a P                      (*  a.P ─a→ P       *)
  | tsuml: ∀P,Q,R,a.                                      (*  P+Q ─a→ P'      *)
                 trans L A P a R → trans L A (P+Q) a R
  | tsumr: ∀P,Q,R,a.                                      (*  P+Q ─a→ Q'      *)
                 trans L A Q a R → trans L A (P+Q) a R
  | tparl: ∀P,Q,R,a.                                      (*  P|Q ─a→ P'|Q    *)
                 trans L A P a R → trans L A (P│Q) a (R│Q)
  | tparr: ∀P,Q,R,a.                                      (*  P|Q ─a→ P |Q'   *)
                 trans L A Q a R → trans L A (P│Q) a (P│R)
  | tpars: ∀P,Q,R,S,a,b.
                 trans L A P a R → trans L A Q b S        (*  P|Q ─τ→ P |Q'   *)
                 → eqact L a (coact L b) → trans L A (P│Q) τ (R│S)
  | tres:  ∀P,R,a,x.                                    (*  P\{b} ─a→ P'\{b}  *)
                 trans L A P a R → And (Not (eqact L a (ava L x)))
                 (Not (eqact L a (coact L (ava L x)))) → trans L A (P〘x〙) a (R〘x〙)
  | trel:  ∀P,R,a,x,b.
                 trans L A P a R                        (*  P[f] ─f(a)→ P'[f] *)
                 → trans L A (P⌊x▹b⌋) (rewact L a b x) (R⌊x▹b⌋)
  | tdef:  ∀P,R,K,a.                                    (*     K ─a→ P'       *)
                 trans L A P a R → K=P → trans L A K a R.



(* <<< Derivatives >>> *)
inductive wderiv (L:Type[0]) (A:act L): proc L A → act L → proc L A → Prop ≝
    eps: ∀p.        wderiv L A p τ p
  | ws : ∀p,a,q.    trans L A p a q → wderiv L A p a q
  | wtl: ∀p,p',a,q. trans L A p τ p' → wderiv L A p' a q → wderiv L A p a q
  | wtr: ∀p,a,q,q'. trans L A q' τ q → wderiv L A p a q' → wderiv L A p a q.

inductive deriv (L:Type[0]) (A:act L): proc L A → act L → proc L A → Prop ≝
    sin: ∀p,a,q.    trans L A p a q → deriv L A p a q
  | tl : ∀p,p',a,q. trans L A p τ p' → deriv L A p' a q → deriv L A p a q
  | tr : ∀p,a,q,q'. trans L A q' τ q → deriv L A p a q' → deriv L A p a q.


lemma deriv_to_wderiv: ∀L,A.∀p,a,p'. deriv L A p a p' → wderiv L A p a p'.
#L #A #p #a #p' #H elim(H) /2 by ws, wtl, wtr/
qed.

lemma wderiv_to_deriv: ∀L,A.∀p,a,p'. wderiv L A p a p' → (Not (a = τ)) →
                                     deriv L A p a p'.
#L #A #p #a #p' #H elim(H) /3 by tnil, sin, tl, tr/
qed.

lemma wderiv_taul: ∀L,A.∀p,p',p'',a. wderiv L A p τ p' → wderiv L A p' a p'' →
                                     wderiv L A p a p''.
#L #A
cut (∀p,a,p'. wderiv L A p a p' → (a = τ) →
     ∀p'',b. wderiv L A p' b p'' → wderiv L A p b p'')
  [ #p #a #p' #H1 elim(H1) /3 by wtl/
  | #Hcut #p #p' #p'' #a #H3 #H4 @(Hcut … τ) //
  ]
qed.

lemma wderiv_taur: ∀L,A.∀p,p',p'',a. wderiv L A p a p' → wderiv L A p' τ p'' →
                                     wderiv L A p a p''.
#L #A
cut (∀p',a,p''. wderiv L A p' a p'' → a = τ →
     ∀p,b. wderiv L A p b p' → wderiv L A p b p'')
  [ #p #a #p' #H1 elim(H1) /3 by wtr/
  | #Hcut #p #p' #p'' #a #H2 #H3 @(Hcut … τ) //
  ]
qed.

lemma wderiv_to_deriv_taul: ∀L,A.∀p,p',p'',a. wderiv L A p τ p' →
                                              deriv L A p' a p'' →
                                              deriv L A p a p''.
#L #A
cut (∀p,a,p'. wderiv L A p a p' → a = τ →
     ∀p'',b. deriv L A p' b p'' → deriv L A p b p'')
  [ #p #a #p' #H1 elim(H1) /3 by tl/
  | #Hcut #p #p' #p'' #a #H2 #H3 @(Hcut … τ) //
  ]
qed.

lemma wderiv_to_deriv_taur: ∀L,A.∀p,p',p'',a. deriv L A p a p' →
                                              wderiv L A p' τ p'' →
                                              deriv L A p a p''.
#L #A
cut (∀p',a,p''. wderiv L A p' a p'' → a = τ →
     ∀p,b. deriv L A p b p' → deriv L A p b p'')
  [ #p' #a #p'' #H1 elim(H1) /3 by tr/
  | #Hcut #p #p' #p'' #a #H2 #H3 @(Hcut … τ) //
  ]
qed.

lemma deriv_taul: ∀L,A.∀p,p',p'',a. deriv L A p τ p' → deriv L A p' a p'' →
                                    deriv L A p a p''.
#L #A #p #p' #p'' #a #H1 #H2 /3 by deriv_to_wderiv, wderiv_to_deriv_taul/
qed.

lemma deriv_taur: ∀L,A.∀p,p',p'',a. deriv L A p a p' → deriv L A p' τ p'' →
                                    deriv L A p a p''.
#L #A #p #p' #p'' #a #H1 #H2 /3 by deriv_to_wderiv, wderiv_to_deriv_taur/
qed.

lemma trans_to_deriv: ∀L,A.∀p,a,p'.∀t1,t2. deriv L A p τ t1 ∧
                                           trans L A t1 a t2 ∧
                                           deriv L A t2 τ p' →
                                           deriv L A p a p'.
#L #A #p #a #p' #t1 #t2 * * #D1 #T #D2
cut(∀p,t1,t2,p'. deriv L A p τ t1 → deriv L A t2 τ p' →
    ∀a. trans L A t1 a t2 → deriv L A p a p')
  [ #p0 #t10 #t20 #p0' #d1 #d2 #a0 #Tt0
    /4 by wderiv_to_deriv_taur, wderiv_to_deriv_taul, deriv_to_wderiv, sin/
  | #Hcut @(Hcut … D1 D2) //
  ]
qed.

lemma deriv_to_trans: ∀L,A.∀p,a,p'.  deriv L A p a p' →
                       ∃b1,t1,b2,t2. (b1=τ) ∧ (b2=τ) ∧
                                     deriv L A p b1 t1 ∧
                                     trans L A t1 a t2 ∧
                                     deriv L A t2 b2 p'.
#L #A #p #a #p' #D elim(D)
  [ #p0 #a0 #p1 #Tp0
    @(ex_intro … τ) @(ex_intro … p0)
    @(ex_intro … τ) @(ex_intro … p1)
    % /2 by sin, tnil/ % // % /2 by sin, tnil/ % //
  | #p0 #p1 #a0 #p2 #Tp0 #Dp1
    * #b1 * #t1 * #b2 * #t2
    * * * * #Eb1 #Eb2 #D1 #T1 #D2
    @(ex_intro … b1) @(ex_intro … t1)
    @(ex_intro … b2) @(ex_intro … t2)
    % // % // % /2 by tl, conj/
  | #p0 #a0 #p2 #p1 #Tp1 #Dp0
    * #b1 * #t1 * #b2 * #t2
    * * * * #Eb1 #Eb2 #D1 #T1 #D2
    @(ex_intro … b1) @(ex_intro … t1)
    @(ex_intro … b2) @(ex_intro … t2)
    % /2 by tr/ % // % /2/
  ]
qed.

lemma trans_to_wderiv: ∀L,A.∀p,a,p'.∀t1,t2. wderiv L A p τ t1 ∧
                                            trans L A t1 a t2 ∧
                                            wderiv L A t2 τ p' →
                                            wderiv L A p a p'.
#L #A #p #a #p' #t1 #t2 * * #W1 #T #W2
cut(∀p,t1,t2,p'. wderiv L A p τ t1 → wderiv L A t2 τ p' →
    ∀a. trans L A t1 a t2 → wderiv L A p a p')
  [ #p0 #t10 #t20 #p0' #w1 #w2 #a0 #Tt0
    /4 by wderiv_taur, wderiv_taul, ws/
  | #Hcut @(Hcut … W1 W2) //
  ]
qed.

lemma wderiv_to_trans: ∀L,A.∀p,a,p'. wderiv L A p a p' →
                       ∃b1,t1,b2,t2. (b1=τ) ∧ (b2=τ) ∧
                                     wderiv L A p b1 t1 ∧
                                     trans L A t1 a t2 ∧
                                     wderiv L A t2 b2 p'.
#L #A #p #a #p' #W elim(W)
  [ #p0
    @(ex_intro … τ) @(ex_intro … p0)
    @(ex_intro … τ) @(ex_intro … p0)
    % // % // % // /2 by eps, conj/
  | #p0 #a0 #p1 #Tp0
    @(ex_intro … τ) @(ex_intro … p0)
    @(ex_intro … τ) @(ex_intro … p1)
    % // % // % // /2 by conj/
  | #p0 #p1 #a0 #p2 #Tp0 #Wp1
    * #b1 * #t1 * #b2 * #t2
    * * * * #Eb1 #Eb2 #W1 #T1 #W2
    @(ex_intro … b1) @(ex_intro … t1)
    @(ex_intro … b2) @(ex_intro … t2)
    % // % // % /2 by wtl, conj/
  | #p0 #a0 #p2 #p1 #Tp1 #Wp0
    * #b1 * #t1 * #b2 * #t2
    * * * * #Eb1 #Eb2 #W1 #T1 #W2
    @(ex_intro … b1) @(ex_intro … t1)
    @(ex_intro … b2) @(ex_intro … t2)
    % /2 by wtr/ % // % /2 by conj/
  ]
qed.



(* <<< Strong equivalence >>> *)
coinductive strong_eq (L:Type[0]) (A:act L): proc L A → proc L A → Prop ≝
  str_eq: ∀p,q.
          (∀a,p'. trans L A p a p' → ∃q'. trans L A q a q' ∧ strong_eq L A p' q') →
          (∀a,q'. trans L A q a q' → ∃p'. trans L A p a p' ∧ strong_eq L A p' q') →
          strong_eq L A p q.


(* Reflexivity *)
let corec ref_streq (L:Type[0]) (A:act L): ∀p. strong_eq L A p p ≝ ?.
#p1 % [ 1,2: #a0 #p2 #Tp @(ex_intro … p2) % // ]
qed.

(* Symmetry *)
let corec sym_streq (L:Type[0]) (A:act L) (p,q:proc L A)
                    (Hse: strong_eq L A p q): strong_eq L A q p ≝ ?.
cases(Hse) #pp #qq #Hp #Hq %
  [ #a #qq' #Tq cases(Hq a qq' Tq) #pp' * #Tp #Hse' @(ex_intro … pp') %
    [ // | @sym_streq // ]
  | #a #pp' #Tp cases(Hp a pp' Tp) #qq' * #Tq #Hse' @(ex_intro … qq') %
    [ // | @sym_streq // ]
  ]
qed.

(* Transitivity *)
let corec trx_streq (L:Type[0]) (A:act L) (p,q,r:proc L A)
                    (Hse1: strong_eq L A p q) (Hse2: strong_eq L A q r):
                    strong_eq L A p r ≝ ?.
inversion(Hse1) #p0 #q0 #Hp #Hq #Epp0 #Eqq0
inversion(Hse2) #t0 #r0 #Ht #Hr #Eqt0 #Err0 %
  [ #a #p1 #Tp
    cases(Hp a p1 Tp) #q1 * #Tq #HseA
    cases(Ht a q1 ?) // #r1 * #Tr #HseB
    @(ex_intro … r1) % [ // | @trx_streq // ]
  | #a #r1 #Tr
    cases(Hr a r1 Tr) #t1 * #Tt #HseB
    cases(Hq a t1 ?) // #p1 * #Tp #HseA
    @(ex_intro … p1) % [ // | @trx_streq // ]
  ]
qed.



(* <<< Weak equivalence >>> *)
coinductive weak_eq (L:Type[0]) (A:act L): proc L A → proc L A → Prop ≝
  wk_eq: ∀p,q.
         (∀a,p'. trans L A p a p' → ∃q'. wderiv L A q a q' ∧ weak_eq L A p' q') →
         (∀a,q'. trans L A q a q' → ∃p'. wderiv L A p a p' ∧ weak_eq L A p' q') →
         weak_eq L A p q.


(* Reflexivity *)
let corec rfl_wkeq (L:Type[0]) (A:act L): ∀p. weak_eq L A p p ≝ ?.
  #p1 % [ 1,2: #a0 #p2 #Tp @(ex_intro … p2) % /2 by ws/ ]
qed.

(* Simmetry *)
let corec sym_wkeq (L:Type[0]) (A:act L) (p,q:proc L A)
                   (Hse: weak_eq L A p q): weak_eq L A q p ≝ ?.
cases(Hse) #pp #qq #Hp #Hq %
  [ #a #qq' #Tq cases(Hq a qq' Tq) #pp' * #Wdp #Hse' @(ex_intro … pp') %
    [ // | @sym_wkeq // ]
  | #a #pp' #Tp cases(Hp a pp' Tp) #qq' * #Wdq #Hse' @(ex_intro … qq') %
    [ // | @sym_wkeq // ]
  ]
qed.

(* Transitivity *)
lemma Htrx_wk: ∀L,A.∀q,q',r,a. wderiv L A q a q' →
                               weak_eq L A q r →
                               ∃r'. wderiv L A r a r' ∧ weak_eq L A q' r'.
#L #A #q #q' #r #a #Wq generalize in match r; -r elim(Wq)
  [ #p #r #Wepr @(ex_intro … r) % //
  | #p #a0 #p' #Tp #r #Wepr inversion(Wepr) #p0 #q0 #Hp #Hq #Epp #Erq
    destruct @(Hp a0 p' Tp)
  | #p #p' #a0 #q0 #Tp #Wdp #Hind #r #Wepr
    cut(∃r''. wderiv L A r τ r'' ∧ weak_eq L A p' r'')
      [ inversion(Wepr) #p0 #q1 #Hp0 #Hq1 #Epp0 #Erq1 destruct @(Hp0 τ p' Tp)
      | * #r'' * #Tr #Wepr'
        cut(∃r'. wderiv L A r'' a0 r' ∧ weak_eq L A q0 r')
          [ @(Hind r'') //
          | * #r' * #Wdr #Weqr
            @(ex_intro … r') % [ /2 by wderiv_taul/ | // ]
          ]
      ]
  | #p #a0 #q0 #q0' #Tq #Wdp #Hind #r #Wepr
    cut(∃r''. wderiv L A r a0 r'' ∧ weak_eq L A q0' r'')
      [ @(Hind r Wepr)
      | *  #r'' * #Wdr #Weqr
        cut(∃r'. wderiv L A r'' τ r' ∧ weak_eq L A q0 r')
          [ inversion(Weqr) #p0 #q1 #Hq0 #Hq1 #Epp0 #Erq1 destruct @(Hq0 τ q0 Tq)
          | * #r' * #Wdr' #Weqr'
            @(ex_intro … r') % [ /2 by wderiv_taur/ | // ]
          ]
      ]
  ]
qed.

let corec trx_wkeq (L:Type[0]) (A:act L) (p,q,r:proc L A)
                   (Hwe1: weak_eq L A p q) (Hwe2: weak_eq L A q r):
                    weak_eq L A p r ≝ ?.
inversion(Hwe1) #p0 #q0 #Hp #Hq #Epp0 #Eqq0
inversion(Hwe2) #t0 #r0 #Ht #Hr #Eqt0 #Err0 %
  [ #a #p1 #Tp cases(Hp a p1 Tp) #q1 * #Wdq #Wepq
    cut(∃r1. wderiv L A r0 a r1 ∧ weak_eq L A q1 r1)
      [ @(Htrx_wk L A q0 q1 r0) //
      | * #r1 * #Wdr #Weqr @(ex_intro … r1) %
          [ // | @trx_wkeq // ]
      ]
  | #a #r1 #Tr cases(Hr a r1 Tr) #t1 * #Wdt #Wetr
    cut(∃p1. wderiv L A p0 a p1 ∧ weak_eq L A t1 p1)
      [ @(Htrx_wk L A t0 t1 p0 a) /2 by sym_wkeq/
      | * #p1 * #Wdp #Wetp @(ex_intro … p1) %
          [ // | @(trx_wkeq … t1) /2 by sym_wkeq/ ]
      ]
  ]
qed.


(* Strong ==> Weak *)
let corec strong_to_weak (L:Type[0]) (A:act L) (p,q:proc L A)
                         (Hs:strong_eq L A p q): weak_eq L A p q ≝ ?.
inversion(Hs) #p0 #q0 #Hp #Hq #Epp0 #Eqq0 %
  [ #a #p1 #Tp cases(Hp a p1 Tp) #q1 * #Tq #Hs1
    @(ex_intro … q1) % [ /2 by ws/ | @strong_to_weak // ]
  | #a #q1 #Tq cases(Hq a q1 Tq) #p1 * #Tp #Hs1
    @(ex_intro … p1) % [ /2 by ws/ | @strong_to_weak // ]
  ]
qed.



(* <<< Very weak equivalence >>> *)
coinductive vweak_eq (L:Type[0]) (A:act L): proc L A → proc L A → Prop ≝
  wk_eq: ∀p,q.
         (∀a,p'. deriv L A p a p' → ∃q'. wderiv L A q a q' ∧ vweak_eq L A p' q') →
         (∀a,q'. deriv L A q a q' → ∃p'. wderiv L A p a p' ∧ vweak_eq L A p' q') →
         vweak_eq L A p q.

(* Very Weak ⇒ Weak *)
let corec vweak_to_weak (L:Type[0]) (A:act L) (p,q:proc L A)
                        (Vwe:vweak_eq L A p q):
                        weak_eq L A p q ≝ ?.
inversion(Vwe) #p0 #q0 #Hp #Hq #Epp0 #Eqq0 %
  [ #a #p1 #Tp
    cases(Hp a p1 ?)
    [ #q1 * #Wdq #We1 @(ex_intro … q1) % [ // | @vweak_to_weak // ]
    | /2 by sin/
    ]
  | #a #q1 #Tq
    cases(Hq a q1 ?)
    [ #p1 * #Wdp #We1 @(ex_intro … p1) % [ // | @vweak_to_weak // ]
    | /2 by sin/
    ]
  ]
qed.

(* Weak + Deriv ⇒ Weak *)
lemma weak_eq_deriv_l: ∀L,A.∀p,q. weak_eq L A p q → ∀a,p'. deriv L A p a p' →
                       ∃q'. wderiv L A q a q' ∧ weak_eq L A p' q'.
#L #A #p #q #We #a #p' #Dp generalize in match We; generalize in match q;
elim(Dp) -Dp -We -a -p -p' -q
  [ #p #a #p' #Tp #q #We inversion(We) #p0 #q0 #Hp #Hq #Epp0 #Eqq0
    destruct cases(Hp a p' Tp) #q' * #Wdq0 #We' @(ex_intro … q') % //
  | #p #p1 #a #p' #Ttp #Dp #Hind #q #We
    cut(∃q1. wderiv L A q τ q1 ∧ weak_eq L A p1 q1)
      [ inversion(We) #p0 #q0 #Hp #Hq #Epp0 #Eqq0
        cases(Hp τ p1 ?) // #q1 * #Wdqt #We1 @(ex_intro … q1) % //
      | * #q1 * #Wdtq #We1
        cut(∃q'. wderiv L A q1 a q' ∧ weak_eq  L A p' q')
        [ @(Hind … q1) //
        | * #q' * #Wdq1 #We' @(ex_intro … q') %
          /2 by wderiv_taul/
        ]
      ]
  | #p #a #p' #p1 #Ttp #Dp #Hind #q #We
    cut(∃q1. wderiv L A q a q1 ∧ weak_eq L A p1 q1)
      [ @(Hind … q We)
      | * #q1 * #Wdq #We1
        cut(∃q'. wderiv L A q1 τ q' ∧ weak_eq L A p' q')
          [ inversion(We1) #p0 #q0 #Hp #Hq #Epp0 #Eqq0
            cases(Hp τ p' ?) [ #q' * #Wdq0 #We' @(ex_intro … q') % // | // ]
          | * #q1 * #Wdqt #We' @(ex_intro … q1) %
            /2 by wderiv_taur/
          ]
      ]    
  ]
qed.

lemma weak_eq_deriv_r: ∀L,A.∀p,q. weak_eq L A p q → ∀a,q'. deriv L A q a q' →
                       ∃p'. wderiv L A p a p' ∧ weak_eq L A p' q'.
#L #A #p #q #We #a #q' #Dq
cut(weak_eq L A q p)
  [ /2 by sym_wkeq/
  | #WeS elim(weak_eq_deriv_l L A q p WeS a q' Dq)
    #p' * #Wdp #We' @(ex_intro … p') % /2 by sym_wkeq/
  ]
qed.

(* Weak ⇒ Very Weak *)
let corec weak_to_vweak (L:Type[0]) (A:act L) (p,q:proc L A)
                        (We:weak_eq L A p q):
                        vweak_eq L A p q ≝ ?.
%
  [ #a #p' #Dp
    cut(∃q'. wderiv L A q a q' ∧ weak_eq L A p' q')
      [ elim(weak_eq_deriv_l L A p q We a p' Dp)
        #q' * #Wdq #We' @(ex_intro … q') % //
      | * #q' * #Wdq #We' @(ex_intro … q') %
        [ // | @weak_to_vweak // ]
      ]
  | #a #q' #Dq
    cut(∃p'. wderiv L A p a p' ∧ weak_eq L A p' q')
      [ elim(weak_eq_deriv_r L A p q We a q' Dq)
        #p' * #Wdp #We' @(ex_intro … p') % //
      | * #p' * #Wdp #We' @(ex_intro … p') %
        [ // | @weak_to_vweak // ]
      ]
  ]
qed.

(* Strong ==> Very Weak *)
let corec strong_to_vweak (L:Type[0]) (A:act L) (p,q:proc L A)
                          (Hs:strong_eq L A p q): vweak_eq L A p q ≝ ?.
cut(weak_eq L A p q)
  [ /2 by strong_to_weak/
  | #Hw %
      [ #a #p' #Dp
        cut(∃q'. wderiv L A q a q' ∧ weak_eq L A p' q')
          [ elim(weak_eq_deriv_l L A p q Hw a p' Dp)
            #q' * #Wdq #We' @(ex_intro … q') % //
          | * #q' * #Wdq #We' @(ex_intro … q') %
            [ // | @weak_to_vweak // ]
          ]
      | #a #q' #Dq
        cut(∃p'. wderiv L A p a p' ∧ weak_eq L A p' q')
          [ elim(weak_eq_deriv_r L A p q Hw a q' Dq)
            #p' * #Wdp #We' @(ex_intro … p') % //
          | * #p' * #Wdp #We' @(ex_intro … p') %
            [ // | @weak_to_vweak // ]
          ]
      ]
  ]
qed.